Repository navigation
fix(lean,#17357): Lean-16d -- deux affirmations fausses (axiomes, exercice 3) - #20124
Conversation
…rcice 3) Cellule 24 : la section 9 annoncait « les theoremes ci-dessus ne dependent d'aucun axiome cache ». La sortie committee de la cellule 25 -- imprimee juste en dessous -- montre le contraire : `blinker_period_two` depend de `blinker_period_two._native.native_decide.ax_1`. Le texte est remplace par l'annonce exacte (trois theoremes fermes par `decide`, un par `native_decide`, `#print axioms` montre la difference). Cellule 34 : l'enonce de l'exercice 3 demandait de definir « le pulsar miniature » et de verifier qu'il est de periode 2, alors que l'anti-piege de la cellule 36 rappelle que ce meme pulsar est de periode 3 et ne peut pas satisfaire `evolve _ 2` -- l'enonce etait insatisfaisable. Le mot « pulsar » n'apparait nulle part ailleurs dans le carnet et aucune figure n'est fournie. L'enonce demande desormais un oscillateur de periode 2, ce que le titre de la section annoncait deja. Les deux cellules sont markdown : exception C.2 (modifs uniquement markdown), aucune re-execution due. Les sorties commitees etaient deja justes -- c'est le texte qui ne l'etait pas. See #17357 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
[ADJOINT PREFLIGHT] READY — attestation tierce a la tete
Commentaire tierce de prevalidation — n'approuve ni ne merge. Lane emettrice : myia-po-2023:CoursIA (file c2142). |
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
Relu a la tete exacte. Deux cellules markdown, source seule. La prose s'aligne sur la sortie #print axioms de la cellule 25 (decide sans axiome, native_decide avec) ; l'exercice 3 ne demande plus un pulsar de periode 2. Exception C.2. B.0 rc=0.
2 participants
Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-lean #20123
Deux affirmations fausses dans
Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb— troisième carnet de la file #17357 pour cette lane.Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (2 constats, 0 faux positif). Audit source : commentaire 5845151383 (Hermes, campagne #17073 —
stale-claimF1,exercise-mismatchF2 ; l'audit conclut lui-même « proposés 2 · confirmés 2 · rejetés 0 · organes 6/6 », et « RAS par ailleurs »).Diff : 2 insertions, 2 suppressions, 2 cellules markdown.
Constat 1 — « aucun axiome caché » (CONFIRMÉ)
La cellule markdown 24 (
87f68042, section 9 « La frontière du prouvé : transparence ») affirmait :La cellule code 25 (
ff5993c8,execution_count: 9) imprime juste en dessous, dans la sortie committée :Le second théorème dépend d'un axiome. L'affirmation était donc fausse, et le carnet se contredisait à une cellule d'intervalle — la promesse (« aucun axiome ») était démentie par sa propre preuve, trois lignes plus bas.
Correctif — le texte annonce désormais ce que la sortie montre, et pourquoi les deux tactiques ne se comportent pas pareil :
Le paragraphe « Pourquoi cela compte-t-il ? » qui suit — celui qui explique ce qu'est une ancre de confiance et pourquoi
#print axiomsdistingue une formalisation d'un test — est conservé intégralement : c'est lui qui donne son sens à la révélation. Un lecteur qui suit la section de bout en bout voit maintenant une question, puis la réponse mesurée (un théorème propre, un théorème porteur de l'axiomenative_decide).Constat 2 — l'exercice 3 était insatisfaisable (CONFIRMÉ)
Cellule markdown 34 (
ac9c83a3), titre « ### Exercice 3 — Un nouvel oscillateur » :Cellule markdown 36 (
d16-attendu-ex3), l'anti-piège de ce même exercice :L'énoncé demandait de vérifier qu'une figure de période 3 est de période 2, et l'anti-piège deux cellules plus loin avertissait précisément que c'est impossible. Un étudiant qui suivait l'énoncé à la lettre était conduit dans le piège que le carnet lui tendait — sans qu'aucune figure intermédiaire ne lui permette de s'en apercevoir : le mot « pulsar » n'apparaît que dans ces deux cellules, et le carnet ne fournit aucune image de pulsar.
Correctif — l'énoncé demande ce que le titre de la section annonçait déjà (« Un nouvel oscillateur ») et ce que l'anti-piège peut alors sanctionner :
La cellule 36 est laissée intacte : son rôle est de nommer le pulsar comme le piège (une figure de période 3 qui ne satisfait pas
evolve _ 2), et ce rôle devient cohérent — et pédagogiquement utile — dès lors que l'énoncé ne demande plus de le construire.Portée du diff
Deux cellules markdown (indices 24 et 34) — les seules touchées :
Vérifié champ par champ contre
HEADsur les 38 cellules :ids,outputs,execution_count,metadataetcell_typeinchangés — 2 champs modifiés au total, tous deux dessource.Aucune ré-exécution due : les deux corrections sont des cellules markdown (exception C.2 explicite). Les sorties committées — dont celle de la cellule 25, qui imprime l'axiome — étaient déjà justes ; c'est le texte qui ne l'était pas. Aucune sortie n'a été éditée à la main.
Observation non demandée (hors périmètre)
Le carnet porte 12 cellules de code avec des
execution_countcontigus1..12et aucune sortie de typeerror— les deux constats de l'audit sont purement rédactionnels, ce qui confirme qu'ils avaient échappé aux gardes mécaniques.See #17357— la file de cette lane compte 11 carnets ; ceci en traite 3 (Lean-11 en #20122, Lean-16a en #20123). Les 8 autres suivent en PR séparées ([RELEASED]à la dernière).🤖 Generated with Claude Code